#pragma once

#include <string>
#include <vector>
#include <map>
#include <list>
#include <set>
#include <algorithm>

#include <tr1/unordered_map>
#include <tr1/unordered_set>

#include <boost/algorithm/string.hpp>
#include <boost/algorithm/string/join.hpp>
#include <boost/lexical_cast.hpp>

#include <time.h>
#include <sys/time.h>
#include <iostream>

#include <math.h>
#include <stdarg.h>

#include "ilp.hpp"
#include "variable_manager.hpp"

#define DATE         { time_t t; tm *p_ltm; static string weekday[] = { "Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat" }; time( &t ); p_ltm = localtime( &t ); cerr << format( "[%02d/%02d/%04d (%s) %02d:%02d:%02d]" ) % (1+p_ltm->tm_mon) % (p_ltm->tm_mday) % (1900+p_ltm->tm_year) % weekday[p_ltm->tm_wday] % p_ltm->tm_hour % p_ltm->tm_min % p_ltm->tm_sec << " "; }
#define DATE2(o)     { time_t t; tm *p_ltm; static string weekday[] = { "Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat" }; time( &t ); p_ltm = localtime( &t ); o << format( "[%02d/%02d/%04d (%s) %02d:%02d:%02d]" ) % (1+p_ltm->tm_mon) % (p_ltm->tm_mday) % (1900+p_ltm->tm_year) % weekday[p_ltm->tm_wday] % p_ltm->tm_hour % p_ltm->tm_min % p_ltm->tm_sec << " "; }
#define WHISPER(v,x) if( g_verbose_level >= v ) { DATE; cerr << x; };
#define WHISPER2(o,v,x) if( g_verbose_level >= v ) { DATE2(o); o << x; };
#define SWHISPER(v,x) if( g_verbose_level >= v ) { cerr << x; };
#define IFWHISPER(v) if( g_verbose_level >= v )

#define foreach(t, v, i) for( t::iterator v = (i).begin(); (i).end() != v; ++v )
#define foreachbw(t, v, b, e) for( t::iterator v = b; e != v; ++v )
#define rforeach(t, v, i) for( t::reverse_iterator v = (i).rbegin(); (i).rend() > v; ++v )
#define foreachc(t, v, i) for( t::const_iterator v = (i).begin(); (i).end() != v; ++v )
#define rforeachc(t, v, i) for( t::const_reverse_iterator v = (i).rbegin(); (i).rend() > v; ++v )

#define NH_OPT 0.01
 
#define UNBOUND_VARIABLE_PREFIX "ub"
#define NEGATION_CHAR           '-'
#define NEGATION_STR            "-"

#define IS_INT(x)               (fabs(fabs(x) - floor(fabs(x) + 0.5)) <= 1e-5)
#define IS_CONST(p)             ('A' <= g_vm.p2v(p)[0] && g_vm.p2v(p)[0] <= 'Z')
#define IS_UNBOUND(p)           (0 == g_vm.p2v(p).find(UNBOUND_VARIABLE_PREFIX))

using namespace std;
using namespace std::tr1;
using namespace boost;

/* General types. */
typedef vector<string>              string_list_t;
typedef unordered_set<string>       string_set_t;
typedef pair<string,string>         string_pair_t;

typedef unordered_set<int>          int_set_t;
typedef vector<int>                 int_list_t;
typedef pair<int, int>              int_pair_t;
typedef vector<int_pair_t>          int_pair_list_t;

typedef unordered_map<int, string_list_t>     isl_dict_t;
typedef unordered_map<int, int_list_t>        iil_dict_t;
typedef unordered_map<int, int_set_t>         iiset_dict_t;
typedef unordered_map<string, iil_dict_t>     siil_dict_t;

typedef unordered_map<int, string>             is_dict_t;
typedef unordered_map<string, int>             si_dict_t;
typedef unordered_map<string, si_dict_t>       ssi_dict_t;
typedef unordered_map<string, string>          ss_dict_t;
typedef map<string, string>                    ss_ordered_dict_t;
typedef unordered_map<string, string_list_t>   ssl_dict_t;
typedef unordered_map<string, string_set_t>    sss_dict_t;
typedef unordered_map<string, int_list_t>      sil_dict_t;
typedef unordered_map<string, int_set_t>       siset_dict_t;
typedef unordered_map<string, sil_dict_t>      ssil_dict_t;
typedef unordered_map<string, ssl_dict_t>      sssl_dict_t;

typedef unordered_map<string, unordered_map<int, string_list_t > >     sisl_dict_t;
typedef unordered_map<int, int >                                       ii_dict_t;
typedef unordered_map<int, unordered_map<int, int> >                   iii_dict_t;
typedef unordered_map<int, unordered_map<int, string> >                iis_dict_t;

typedef unordered_map<string, ii_dict_t>       sii_dict_t;

/* Prototypes. */
namespace ie { class variable_cluster_t; };
namespace kb { class pool_t; };

struct unifier_t;
struct literal_t;
struct progress_bar_t;

/* Aim-specific types. */
enum literal_repr_t { Default, OrgArgs, LiteralOrgArgs, Literal, PredicateArity };
enum graph_repr_t { SimpleGraph, ComplexGraph, FullGraph };

typedef unordered_set<literal_t*>              literal_pset_t;
typedef list<literal_t*>                       literal_plist_t;
typedef vector<literal_t*>                     literal_pvector_t;

typedef unordered_map<string, int_set_t>       slps_dict_t;
typedef unordered_map<string, int_list_t>      slpl_dict_t;

typedef size_t axiom_t;
typedef vector<axiom_t> axiom_list_t;

/* Globals. */
extern progress_bar_t     g_progress_bar;
extern variable_manager_t g_vm;
extern int                g_verbose_level;

struct progress_bar_t {
  pthread_t    h_thread;
  unsigned int step, max_step;
  bool         f_active;

  static inline void _draw_bar() {
    static const char* fan = "|/-\\"; static int counter = 0;
    int  step = int(100.0 * ((double)g_progress_bar.step / (double)g_progress_bar.max_step));
    char buffer[1024]; sprintf( buffer, " %c |%s>%s| %3d%% done.", fan[counter++ % 4], string( max(1,step/2), '-' ).c_str(), string(100/2 - step/2, ' ').c_str(), step );
    cerr << buffer << string( strlen( buffer ), '\b' ) << flush;  
  }

  static inline void *_thread_progress_bar( void *p_context ) {
    while( true ) {
      while( g_progress_bar.f_active && g_progress_bar.step <= g_progress_bar.max_step ) {
        _draw_bar();
        usleep(100000); /* 100ms */
      }
      usleep(500000); /* 500ms */
    }
    pthread_exit(NULL);
  }
  
  inline void start_thread() { f_active = false; step = 1; max_step = 100; pthread_create( &h_thread, NULL, _thread_progress_bar, NULL ); }
  inline void kill_thread() { pthread_cancel( h_thread ); }
  inline void wakeup( unsigned int _max_step ) { step = 1; max_step = max( (unsigned int)1, _max_step); f_active = true; }
  inline void goto_school() { step++; }
  inline void goto_hell() { f_active = false; step = max_step; _draw_bar(); cerr << endl; }
  
};

struct literal_t {

  int                 id, group_id, xor_id;
  ilp::variable_t     var_pay, var_reduce;
  ilp::constraint_t   con_r1, con_r2, con_r3, con_and;
  string              predicate, generated_by, named, merged_with;
  logvar_list_t       arguments, o_arguments;
  axiom_list_t        applied_axioms;
  vvset_dict_t        axiom_substitution;
  double              number, number_sibling, number_benefit;
  int_set_t           parents, ancestor, ancestor_repr, children, sibling;
  int_set_t           unified_with, xor_path;
  int                 fixed_value, last_applied_axiom;
  list<unifier_t>     conditions;

  literal_t           *p_absorbed_by;
  
  bool                is_hypothesized, is_reduced, is_observed, is_eob, is_absorbed;
  bool                is_discarded;

  literal_t() : 
    p_absorbed_by(NULL), fixed_value(-1), number(0.0), number_benefit(0.0), xor_id(-1),
    is_observed(false), is_absorbed(false), is_eob(false), is_discarded(false),
    con_r1(ilp::INVALID_HANDLE), con_r2(ilp::INVALID_HANDLE), con_r3(ilp::INVALID_HANDLE),
    con_and(ilp::INVALID_HANDLE) {}
  
  string to_string( literal_repr_t = Default ) const;
  
};

class literal_list_t : public list<literal_t> {
public:
  string to_string() const;
};

class literal_vector_t : public vector<literal_t> {
public:
  string to_string() const;
};

struct unifier_operator_t;
struct unifier_t {

  int                id;
  unifier_operator_t *p_operator;
  ilp::variable_t    var_operator;
  int                argument;
  int                constrain_type;
  logical_variable_t v1, v2;
  bool               is_applied;

  unifier_t() : constrain_type(0), is_applied(false), var_operator(ilp::INVALID_HANDLE), v1(-1), v2(-1) {}
  unifier_t( const logical_variable_t &_v1, const logical_variable_t &_v2 ) : constrain_type(0), is_applied(false), var_operator(ilp::INVALID_HANDLE), v1(_v1), v2(_v2) {}
  unifier_t( const logical_variable_t &_v1, const logical_variable_t &_v2, ilp::variable_t _var_operator ) : constrain_type(0), is_applied(false), var_operator(_var_operator), v1(_v1), v2(_v2) {}

  inline string to_string() const { return g_vm.p2v( v1 ) + "=" + g_vm.p2v( v2 ); }

  inline void set( unifier_t& u ) {
    var_operator   = u.var_operator; v1 = u.v1; v2 = u.v2;
    constrain_type = u.constrain_type; is_applied = u.is_applied;
  }
  
};

class unifier_list_t : public list<unifier_t> {
public:
  string to_string() const;
};

struct unifier_operator_t {

  int                         h1, h2;
  ilp::variable_t             var_operator;
  bool                        is_applied, is_postponed;
  ilp::constraint_t           con_u1, con_u2, con_u3, con_e;
  vector<ilp::variable_set_t> constraints;
  int_list_t                  unifiers;

  unifier_operator_t() : h1(-1), h2(-1), is_postponed(false), is_applied(false), var_operator(ilp::INVALID_HANDLE), con_u1(ilp::INVALID_HANDLE), con_u2(ilp::INVALID_HANDLE), con_u3(ilp::INVALID_HANDLE), con_e(ilp::INVALID_HANDLE) {}
  unifier_operator_t( ilp::variable_t _var_operator ) : h1(-1), h2(-1), is_postponed(false), is_applied(false), var_operator(_var_operator), con_u1(ilp::INVALID_HANDLE), con_u2(ilp::INVALID_HANDLE), con_u3(ilp::INVALID_HANDLE), con_e(ilp::INVALID_HANDLE) {}
  
  string to_string( const unifier_t *p_storage ) const;
  
};

typedef unordered_map<string, unifier_t>              unifier_map_t;
typedef unordered_map<string, unifier_map_t>          unifier_dict_t;

typedef unordered_map<int, unifier_operator_t>        iu_dict_t;
typedef unordered_map<int, iu_dict_t>                 unified_literal_dict_t;


/* Utility functions. */
#define has_key( dict, key ) (dict.end() != dict.find( key ))

inline double gettimeofday_sec()  {
  timeval tv;
  gettimeofday(&tv, NULL);
  return tv.tv_sec + (double)tv.tv_usec*1e-6;
}
  
template <class I> inline string awesome_join( I begin, I end ) {
  string_list_t sl;
  for( I itr = begin; end != itr; ++itr )
    sl.push_back( lexical_cast<string>( *itr ) );
  return join( sl, "," );
}

inline bool has_common( const int_set_t &s1, const int_set_t &s2 ) {
  foreachc( int_set_t, iter_s1, s1 ) {
    foreachc( int_set_t, iter_s2, s2 ) {
      if( *iter_s1 == *iter_s2 ) return true;
    } }
  return false;
}

